Inference at * 2 1 1 
Iof proof for Lemma member nth tl:

.....equality..... NILNIL

1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
5. T
6. T List
  nth_tl(n;[]) = [] 

latex

 by Assert n:. nth_tl(n;[]) = [] 

latex

 1: .....assertion..... NILNIL

 1:   n:. nth_tl(n;[]) = []
 2: 

 2: 7. n:. nth_tl(n;[]) = []
 2:   nth_tl(n;[]) = []
 .

Definitions

x:A. B(x), , s = t, type List, nth_tl(n;as), []